T:Type, L:(T List), x, y:T.
no_repeats(T;L)  adjacent(T;L;x;y)  (z:T. z before y  L  (z before x  L  (z = x))) 

latex

ProofTree

Definitions

t  T, type List, A List, s = t, x:AB(x), x:A. B(x), [car / cdr], no_repeats(T;l), Type, adjacent(T;L;x;y), x before y  l, left + right, P  Q, P  Q, [], False, ||as||, a < b, hd(l), x:A  B(x), P & Q, P  Q, , (x  l), P  Q, Dec(P), A, , A  B, Atom, {i..j}, , b, x,y:A//B(x;y), x:A. B(x), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, A c B, f(a), x f y, |r|, xL. P(x), (xL.P(x)), Unit, x:A.B(x), L1  L2, #$n, {T}, Void

Lemmas

adjacent-member, l before antisymmetry, false wf, not wf, no repeats iff, l before member2, hd-before, no repeats cons, decidable or, decidable cand, or functionality wrt iff, cons before, iff wf, rev implies wf, l member wf, adjacent-cons, adjacent-nil, l before wf, adjacent wf, no repeats wf